
PHP_ARG_ENABLE(EventDispatcher, whether to enable EventDispatcher support,
[  --enable-EventDispatcher           Enable EventDispatcher support])

if test "$PHP_EVENTDISPATCHER" != "no"; then

  PHP_NEW_EXTENSION(EventDispatcher, EventDispatcher.c, $ext_shared)
fi
